COMMENT ⊗   VALID 00003 PAGES
C REC  PAGE   DESCRIPTION
C00001 00001
C00002 00002	facts about lengths of lists
C00004 00003	proofs lengthprop
C00006 ENDMK
C⊗;
;facts about lengths of lists
;10s
(wipe-out)
(get-proofs set)
(get-proofs minus)

(proof length)

(decl length (type: |ground→ground|) (unaryname: length))
(define length |∀u x.(length nil=0)∧length(x.u)=(length u)'|
        (use listinductiondef))
(label simpinfo) (label lengthdef)

(axiom |∀u.natnum(length u)|)
(label simpinfo)

(axiom |∀u.length u=0≡null u|)
(label simpinfo)

(axiom |∀u v.length (u*v)=length u+length v|)
(label lengthadd) (label simpinfo)

(axiom |∀x.length (x.nil)=1|)
(label simpinfo)
 
(axiom |∀u n.length(u)≤n∨n<length(u)|)
(label trichotomy2)

(axiom |∀u y.member(y,u)⊃0<length u|)
(label simpinfo)(label have_member)

(axiom |∀u y.member(y,u)⊃¬null u|)
(label simpinfo)(label have_member1)

(save-proofs length)
;proofs lengthprop
(wipe-out)
(get-proofs length)
(proof lengthprop)
(unlabel simpinfo length#3 length#4 lengthadd length#6 have_member have_member1)

(ue (phi |λu.natnum length u|) listinduction (open length))
;∀U.NATNUM(LENGTH U)
(label simpinfo length#3)

(ue (phi |λu.(length u=0)≡null u|) listinduction
    (open length) (use zero_not_successor))
;∀U.LENGTH U=0≡NULL U
(label simpinfo length#4)

(ue (phi |λu.length(u*v)=length u+length v|) listinduction
    (open append length))
;∀U.LENGTH (U*V)=LENGTH U+LENGTH V
(label simpinfo lengthadd)

(trw |length(x.nil)| (open length))
;LENGTH (X.NIL)=1
(label simpinfo length#6)

(derive |length(u)≤n∨n<length(u)| trichotomy (open lesseq))

(ue (phi |λu.member(y,u)⊃0<length u|) listinduction (open member))
;∀U.MEMBER(Y,U)⊃0<LENGTH U
(label simpinfo have_member)

(ue (phi |λu.member(y,u)⊃¬null u|) listinduction (open member))
;∀U.MEMBER(Y,U)⊃¬NULL U
(label simpinfo have_member1)